#include <iostream>
#include <cstdlib>
#include <cstdio>
#include <cstring>
#include <cassert>

#include <map>
#include <set>
#include <vector>
#include <list>
#include <string>
#include <algorithm>
#include <queue>

//#include <jni.h>
#include "/usr/lib/jvm/java-6-sun-1.6.0.26/include/jni.h"
#include "core/Solver.h"
#include "kodkod_engine_satlab_MiniSat.h"

using namespace Minisat;


/*
 * Class:     kodkod_engine_satlab_MiniSat
 * Method:    make
 * Signature: ()J
 */
JNIEXPORT jlong JNICALL Java_kodkod_engine_satlab_MiniSat_make
  (JNIEnv *, jclass) {
  Solver* solver = new Solver();
  return ((jlong) solver);
}

/*
 * Class:     kodkod_engine_satlab_MiniSat
 * Method:    free
 * Signature: (J)V
 */
JNIEXPORT void JNICALL Java_kodkod_engine_satlab_MiniSat_free
  (JNIEnv *, jobject, jlong solver) {
  delete ((Solver*)solver);  
}

/*
 * Class:     kodkod_engine_satlab_MiniSat
 * Method:    addVariables
 * Signature: (JI)V
 */
JNIEXPORT void JNICALL Java_kodkod_engine_satlab_MiniSat_addVariables
  (JNIEnv *, jobject, jlong solver, jint  numVars) {
  Solver* solverPtr = (Solver*) solver;
  for(int i = 0; i < numVars; ++i) {
     solverPtr->newVar();
  }
}

/*
 * Class:     kodkod_engine_satlab_MiniSat
 * Method:    addClause
 * Signature: (J[I)Z
 */
JNIEXPORT jboolean JNICALL Java_kodkod_engine_satlab_MiniSat_addClause
  (JNIEnv * env, jobject, jlong solver, jintArray clause) {
    jsize length = env->GetArrayLength(clause);
    jint* buf = env->GetIntArrayElements(clause, JNI_FALSE);
    Solver* solverPtr = ((Solver*)solver);
    vec<Lit> lits;
    for(int i = 0; i < length; ++i) {
        int var = *(buf+i);
        lits.push((var > 0) ?  mkLit(var-1) : ~mkLit(-var-1));
    }
    solverPtr->addClause(lits);
    env->ReleaseIntArrayElements(clause, buf, 0);
    return solverPtr->okay();
 }

/*
 * Class:     kodkod_engine_satlab_MiniSat
 * Method:    valueOf
 * Signature: (JI)Z
 */
JNIEXPORT jboolean JNICALL Java_kodkod_engine_satlab_MiniSat_valueOf
  (JNIEnv *, jobject, jlong solver, jint var) {
  return ((Solver*)solver)->model[var-1]==l_True;
 }

static bool _stop = false;

/*
 * Class:     kodkod_engine_satlab_MiniSat
 * Method:    solve
 * Signature: (J)Z
 */
JNIEXPORT jboolean JNICALL Java_kodkod_engine_satlab_MiniSat_solve
  (JNIEnv *, jobject, jlong solver) {
	_stop = false;
	return ((Solver*)solver)->solve();
  }

///*
// * Class:     kodkod_engine_satlab_MiniSat
// * Method:    heapIncreaseVar
// * Signature: (JI)V
// */
//JNIEXPORT void JNICALL Java_kodkod_engine_satlab_MiniSat_heapIncreaseVar
//  (JNIEnv *, jobject, jlong solver, jint id) {
//	((Solver*)solver)->varBumpActivity(id-1);
//}

/*
 * Class:     kodkod_engine_satlab_MiniSat
 * Method:    heapIncreaseVarWithStepSize
 * Signature: (JID)V
 */
JNIEXPORT void JNICALL Java_kodkod_engine_satlab_MiniSat_heapIncreaseVar
  (JNIEnv *, jobject, jlong solver, jint id, jdouble stepsize) {
	((Solver*)solver)->varBumpActivity(id-1, stepsize);
}

/*
 * Class:     kodkod_engine_satlab_MiniSat
 * Method:    heapIncreaseVar
 * Signature: (JI)V
 */
JNIEXPORT void JNICALL Java_kodkod_engine_satlab_MiniSat_heapIncreaseVar2
  (JNIEnv *, jobject, jlong solver, jint id, jint weight) {
	((Solver*)solver)->varTotalOrder(id-1, weight);
}

/*
 * Class:     kodkod_engine_satlab_MiniSat
 * Method:    heapIncreaseVar
 * Signature: (JI)V
 */
JNIEXPORT void JNICALL Java_kodkod_engine_satlab_MiniSat_suggestPolarity
  (JNIEnv *, jobject, jlong solver, jint id, jboolean polarity, jint force) {
	((Solver*)solver)->suggestPolarity(id-1, polarity, force);
}

/*
 * Class:     kodkod_engine_satlab_MiniSat
 * Method:    turnOnRandomVarPicking
 * Signature: (J)V
 */
JNIEXPORT void JNICALL Java_kodkod_engine_satlab_MiniSat_turnOnRandomVarPicking
  (JNIEnv *, jobject, jlong solver) {
	((Solver*)solver)->random_var_freq = 0.2;
}

/*
 * Class:     kodkod_engine_satlab_MiniSat
 * Method:    turnOffRandomVarPicking
 * Signature: (J)V
 */
JNIEXPORT void JNICALL Java_kodkod_engine_satlab_MiniSat_turnOffRandomVarPicking
  (JNIEnv *, jobject, jlong solver) {
	((Solver*)solver)->random_var_freq = 0.0;
}

/*
 * Class:     kodkod_engine_satlab_MiniSat
 * Method:    turnOnRestarts
 * Signature: (J)V
 */
JNIEXPORT void JNICALL Java_kodkod_engine_satlab_MiniSat_turnOnRestarts
  (JNIEnv *, jobject, jlong solver) {
	((Solver*)solver)->restartsEnabled = true;
}

/*
 * Class:     kodkod_engine_satlab_MiniSat
 * Method:    turnOffRestarts
 * Signature: (J)V
 */
JNIEXPORT void JNICALL Java_kodkod_engine_satlab_MiniSat_turnOffRestarts
  (JNIEnv *, jobject, jlong solver) {
	((Solver*)solver)->restartsEnabled = false;
}

/*
 * Class:     kodkod_engine_satlab_MiniSat
 * Method:    getNumberOfConflicts
 * Signature: (J)I
 */
JNIEXPORT jint JNICALL Java_kodkod_engine_satlab_MiniSat_getNumberOfConflicts
  (JNIEnv *, jobject, jlong solver) {
	return (int)((Solver*)solver)->conflicts;
}

/*
 * Class:     kodkod_engine_satlab_MiniSat
 * Method:    getNumberOfDecisions
 * Signature: (J)I
 */
JNIEXPORT jint JNICALL Java_kodkod_engine_satlab_MiniSat_getNumberOfDecisions
  (JNIEnv *, jobject, jlong solver) {
	return (int)((Solver*)solver)->decisions;
}

/*
 * Class:     kodkod_engine_satlab_MiniSat
 * Method:    getNumberOfPropagations
 * Signature: (J)I
 */
JNIEXPORT jint JNICALL Java_kodkod_engine_satlab_MiniSat_getNumberOfPropagations
  (JNIEnv *, jobject, jlong solver) {
	return (int)((Solver*)solver)->propagations;
}

/*
 * Class:     kodkod_analysis_SolverThread
 * Method:    stop
 * Signature: (V)V
 */
JNIEXPORT void JNICALL Java_kodkod_analysis_SolverThread_stopSolver(JNIEnv *env, jobject obj) {
	_stop = true;
}

bool timeout() {
	return _stop;
}
